A:Type, eq:EqDecider(A), B:(AType), f, g:a:A fp B(a), x:A, z:B(x).
f || g  f  g(x)?z = g(x)?f(x)?z  B(x) 

latex

Definitions	t  T, x:A. B(x), b, A, x(s), b, , Prop, f(x), x. t(x), Top, a:A fp B(a), x  dom(f), P  Q, P & Q, P  Q, Unit, if b t else f fi, f  g, P  Q, f(x)?z, f || g, EqDecider(T), False, {T}
Lemmas	fpf-join-ap-sq, fpf-ap wf, fpf-compatible wf, fpf wf, deq wf, not functionality wrt iff, fpf-join-dom, fpf-join wf, top wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, fpf-trivial-subtype-top, bool wf, bnot wf, not wf, assert wf